Frequently the user of a theorem prover "knows" a lot of detail about

the  problem  domain  being axiomatized.   Much  of  this information

(almost by definiton) is  domain-dependent and  thus doesn't  fit the

usual set  of strategies as  well as could  be desired. Also  much of

this information is  heuristic in nature   and would be  difficlut to

express in the form of  axioms.  To help with these problems  we have

introduced two new ideas:  (1) a language for  describing strategies;

and (2) new data types have  been added to LISP so that the  user may

taylor-make his own prover.

The strategy language allows Boolean and conditional expressions over

properties   of  clauses.    Major  extensions   of  this   idea  are

contemplated..

The programmable  aspects allow  the user  to describe   first oreder

statements, strategies and pattern matching in an intuitive notation.

With these facilities inside LISP we can write new rules of inference

and domain dependent theorem provers.



The Language of Strategies.

(1) Choice strategies.

Choice strategies occur in the following context: Given two  possible

candidates,C1  and  C2,  for  the application  of  a  binary  rule of

inference, I, a choice strategy will determine whether not we wish to

form I(C1,C2).

Builtin choice strategies.

a) NONE  allows unrestricted applications of the rules of inference.

b) ANCESTRY implements the AFF  strategy; that is, to apply  I either

C1 or C2  must be an  initial clauses, or,  either C1 appears  in the

derivation tree of C2, or C2 appears in the tree of C1.

c)  SUPPORT  designates the  set-of-support  strategy.  This strategy

basically says that every first-level deduction must have one  of its

parents in the support set.  SUPPORT must be followed by  an argument

list describing which  statements are to be supported.   The elements

of the argument list may either be clause numbers or names  which the

user has associated with certain input clauses.

Example: SUPPORT[1,2,AXIOM[2],THEOREM]  would put clauses  numbered 1

and 2, the  clause AXIOM[2], and all  clauses with name,  THEOREM, in

the support set.

d) VINE strategy says that either C1 or C2 must be an initial clause.

This strategy is known to be incomplete, but is useful in many cases.

For example  it is  easy to  show that  VINE is  complete if  all the



initial statements are either  units(singletons) or  are of  the form

L1∧L2∧...∧Ln ⊃M.

e) UNIT strategy  says that either C1  or C2 are  singletons.  Again,

this strategy  is not complete  ,but is useful  as a  "quick-kill" or

"end-game" strategy.   It is easy  to show that  if there is  a UNIT-

refutation then there is a VINE-form refutation.

f) P1 (P2) is the P1 (P2)-deduction of Robinson. Here it  is required

that either C1 or  C2 contain only positive(negative)  literals. This

strategy is complete.

g) MODEL is the implementation  of a very simple  case of  the model-

relative deduction strategy of Luckham.  Model-relative  deduction is

a generalization of P1  and P2 deduction and is  complete.  Deduction

relative to a model says that at least one of the clauses C1 or C2 be

false  of the  model.  MODEL  expects an  argument list  describing a

binary partition  of the predicate  letters appearing in  the initial

clauses. In the current restricted implementation this says either C1

or  C2  must have  zero  intersection  with the  two  members  of the

partition.

h) DEFMODEL  can be  used to designate  a LISP  function to  define a

model for the current  set of statements.  DEFMODEL expects  a single

argument which is  the name of a  LISP function(of one  argument) and

which implements the defining conditions of a model.

i) EQUALITY signals that the replacement rule, paramodulation,  is to



be  used.   EQUALITY needs  two  arguments: a  predicate  name  to be

interpreted as equality; and  second, a number, called  PDEPTH, which

determines how deep  in the nesting  of function symbols  the matcher

will look in attempting to  match terms.  For example, a PDEPTH  of 1

says only examine primary occurences of terms.



(2) Editing Strategies.

Editing  strategies  are  applied  to the  resluts  of  the  rules of

inference.   These strategies  are used  to  filter  out some  of the

deductions which a rule of inference has generated.

Builtin editing strategies.

a)  DEMOD  is  a  rule  of  simplification  most  commonly   used  in

conjunction  with  EQUALITY.  DEMOD takes  two  arguments.  The first

describes a list of equality units; the second, a number named DDEPTH

which,like PDEPTH, determines a bound on the matching routines.

b) DEPTH takes a single integer argument interpreted to be a bound on

the depth of  function symbol nesting which  must not be  exceeded if

the deduction is to be retained.

For example, DEPTH[4].

c) LENGTH  also takes an  integer argument and  gives a bound  on the

number of literals which will be allowed in any deduction.



Boolean  combinations  of  built-in  or  user-defined  strategies are

allowed.   For example,  a reasonable  choice strategy   is: ancestry

filter form with a set of support being the negation of the statement

to be proved.  This can be written as:

 ANCESTRY ∧ SUPPORT[THEOREM];

An editing strategy which filters out all clauses whose length(number

of literals) is  greater than 4 or  whose depth( depth of  nesting of

function symbols) is greater than 3 can be expressed as:

LENGTH[4] ∨ DEPTH [3];



A programmable theorem prover.

It  is now  possible to  write LISP-like  programs which  control the

actions of  the theroem  prover and  manipulate clauses.   Data types

for CLAUSES, STRATEGIES, and PATTERNS have been added to LISP so that

the user can describe  his clause manipulations in the  same notation

which  is  used  to  drive  the  on-line  prover.    LISP  functions,

ATTEMPTUNTIL and FIND, have been defined to perform controlled proof-

attempts and clause-list searching.

1. Data Types.

a) [CLAUSES <clauses>] is used  to introduce new clause lists  to the

program.  For example: (SETQ X [CLAUSES DSK:FOO])  when executed will

assign to X the  clauselist manufactured from the statements  on file

FOO.

b)   [CHOICE  <strategy>]   and  [EDIT   <strategy>]   introduce  the

appropriate strategies.

c) [PATTERN <pattern>] is  useful in conjunction with FIND  to filter

out  clauses which match <pattern>.

2. Procedures.

(ATTEMPTUNTIL   <clauses><choice-strategy><edit-strategy><termination

condition>)

where: 1) <clauses> is a list of clauses . 2) <choice-strategy>  is a

representation of a  choice strategy.  3)  <edit-strategy> represents

an  editing strategy.   4)  <termination condition>  is  a functional



argument which will be evaluated periodically during the execution of

the  ATTEMPTUNTIL.  As  long as  the condition  evaluated to  NIL the

proof  attempt  will continue.  If  the condition  becomes  true then

ATTEMPTUNTIL will return the  list of all deductions which  have been

made.

For example:

(ATTEMPTUNTIL [CLAUSES  DSK: FOO]  [CHOICE ANCESTRY∧SUPPORT[THEOREM]]

[EDIT LENGTH[4]∨DEPTH[3]] (FUNCTION (LAMBDA()(GREATERP LEVEL 3))) )

will begin  a proof  search using file  DSK:FOO with  choice strategy

being AFF  and supporting  the negation  of the  theorem.  Deductions

whose length is greater than  4 or whose depth of fuction  nesting is

greater than 3 will be discarded.  The proof search will terminate at

the end of level 3.

If a refutation is discovered during any attempt, (QED)  is returned.

If no retutation is found, then the on-line editor is called  to give

the user a chance to examine the current proof environment.  There is

a  third  way  to  exit ATTEMPTUNTIL:  since  the  on-line  editor is

available inside the proof  attempt, typing ABandon <clauses>  to the

editor will force  termination of the  proof attempt and  will return

the selected <clauses>.

(FIND <clauses><pattern>)

where:  1)  <clauses>  is  a list  of  clauses.   2)  <pattern>  is a

condition which is to be applied to each element of <clauses>.



The  value of  FIND is  a  list of  all elements  of  <clauses> which

satisfy the <pattern>.

For example (FIND  XX [PATTERN α(C)=1]) will  find all clauses  in XX

which are units(singletons).